h(e(x), y) → h(d(x, y), s(y))
d(g(g(0, x), y), s(z)) → g(e(x), d(g(g(0, x), y), z))
d(g(g(0, x), y), 0) → e(y)
d(g(0, x), y) → e(x)
d(g(x, y), z) → g(d(x, z), e(y))
g(e(x), e(y)) → e(g(x, y))
↳ QTRS
↳ DependencyPairsProof
h(e(x), y) → h(d(x, y), s(y))
d(g(g(0, x), y), s(z)) → g(e(x), d(g(g(0, x), y), z))
d(g(g(0, x), y), 0) → e(y)
d(g(0, x), y) → e(x)
d(g(x, y), z) → g(d(x, z), e(y))
g(e(x), e(y)) → e(g(x, y))
H(e(x), y) → H(d(x, y), s(y))
D(g(g(0, x), y), s(z)) → G(e(x), d(g(g(0, x), y), z))
H(e(x), y) → D(x, y)
D(g(x, y), z) → D(x, z)
D(g(x, y), z) → G(d(x, z), e(y))
G(e(x), e(y)) → G(x, y)
D(g(g(0, x), y), s(z)) → D(g(g(0, x), y), z)
h(e(x), y) → h(d(x, y), s(y))
d(g(g(0, x), y), s(z)) → g(e(x), d(g(g(0, x), y), z))
d(g(g(0, x), y), 0) → e(y)
d(g(0, x), y) → e(x)
d(g(x, y), z) → g(d(x, z), e(y))
g(e(x), e(y)) → e(g(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
H(e(x), y) → H(d(x, y), s(y))
D(g(g(0, x), y), s(z)) → G(e(x), d(g(g(0, x), y), z))
H(e(x), y) → D(x, y)
D(g(x, y), z) → D(x, z)
D(g(x, y), z) → G(d(x, z), e(y))
G(e(x), e(y)) → G(x, y)
D(g(g(0, x), y), s(z)) → D(g(g(0, x), y), z)
h(e(x), y) → h(d(x, y), s(y))
d(g(g(0, x), y), s(z)) → g(e(x), d(g(g(0, x), y), z))
d(g(g(0, x), y), 0) → e(y)
d(g(0, x), y) → e(x)
d(g(x, y), z) → g(d(x, z), e(y))
g(e(x), e(y)) → e(g(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
G(e(x), e(y)) → G(x, y)
h(e(x), y) → h(d(x, y), s(y))
d(g(g(0, x), y), s(z)) → g(e(x), d(g(g(0, x), y), z))
d(g(g(0, x), y), 0) → e(y)
d(g(0, x), y) → e(x)
d(g(x, y), z) → g(d(x, z), e(y))
g(e(x), e(y)) → e(g(x, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(e(x), e(y)) → G(x, y)
The value of delta used in the strict ordering is 1.
POL(e(x1)) = 1 + x_1
POL(G(x1, x2)) = x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
h(e(x), y) → h(d(x, y), s(y))
d(g(g(0, x), y), s(z)) → g(e(x), d(g(g(0, x), y), z))
d(g(g(0, x), y), 0) → e(y)
d(g(0, x), y) → e(x)
d(g(x, y), z) → g(d(x, z), e(y))
g(e(x), e(y)) → e(g(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
D(g(x, y), z) → D(x, z)
D(g(g(0, x), y), s(z)) → D(g(g(0, x), y), z)
h(e(x), y) → h(d(x, y), s(y))
d(g(g(0, x), y), s(z)) → g(e(x), d(g(g(0, x), y), z))
d(g(g(0, x), y), 0) → e(y)
d(g(0, x), y) → e(x)
d(g(x, y), z) → g(d(x, z), e(y))
g(e(x), e(y)) → e(g(x, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D(g(g(0, x), y), s(z)) → D(g(g(0, x), y), z)
Used ordering: Polynomial interpretation [25,35]:
D(g(x, y), z) → D(x, z)
The value of delta used in the strict ordering is 1/16.
POL(g(x1, x2)) = 0
POL(D(x1, x2)) = (1/4)x_2
POL(s(x1)) = 1/4 + (2)x_1
POL(0) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
D(g(x, y), z) → D(x, z)
h(e(x), y) → h(d(x, y), s(y))
d(g(g(0, x), y), s(z)) → g(e(x), d(g(g(0, x), y), z))
d(g(g(0, x), y), 0) → e(y)
d(g(0, x), y) → e(x)
d(g(x, y), z) → g(d(x, z), e(y))
g(e(x), e(y)) → e(g(x, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D(g(x, y), z) → D(x, z)
The value of delta used in the strict ordering is 1/8.
POL(g(x1, x2)) = 1/4 + (4)x_1
POL(D(x1, x2)) = (1/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
h(e(x), y) → h(d(x, y), s(y))
d(g(g(0, x), y), s(z)) → g(e(x), d(g(g(0, x), y), z))
d(g(g(0, x), y), 0) → e(y)
d(g(0, x), y) → e(x)
d(g(x, y), z) → g(d(x, z), e(y))
g(e(x), e(y)) → e(g(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
H(e(x), y) → H(d(x, y), s(y))
h(e(x), y) → h(d(x, y), s(y))
d(g(g(0, x), y), s(z)) → g(e(x), d(g(g(0, x), y), z))
d(g(g(0, x), y), 0) → e(y)
d(g(0, x), y) → e(x)
d(g(x, y), z) → g(d(x, z), e(y))
g(e(x), e(y)) → e(g(x, y))